Nuprl Lemma : R-interface_wf
11,40
postcript
pdf
A
,
B
:es_realizer{i:l}. R-interface(
A
;
B
)
prop{i:l}
latex
Definitions
x
.
t
(
x
)
,
R-interface(
A
;
B
)
,
prop{i:l}
,
t
T
,
x
:
A
.
B
(
x
)
,
x
(
s
)
Lemmas
es
realizer
wf
,
top
wf
,
ldst
wf
,
rcv
wf
,
Kind-deq
wf
,
lsrc
wf
,
R-da
wf
,
Knd
wf
,
fpf-cap
wf
,
subtype
rel
wf
,
Id
wf
,
IdLnk
wf
origin
A,B:es_realizer{i:l}. R-interface(A; B) 
prop{i:l} A,B:es_realizer{i:l}. R-interface(A; B) prop{i:l} 
x. t(x) Tx:A. B(x)